DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2019.6

Combinations of Qualitative Winning for Stochastic Parity Games

Authors: Krishnendu Chatterjee and Nir Piterman

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract

We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths to satisfy the condition, almost-sure winning, which requires the condition to be satisfied with probability 1, and limit-sure winning, which requires the condition to be satisfied with probability arbitrarily close to 1. We study the combination of two of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et al. for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP cap co-NP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a) we show that for MDPs with finite-memory strategies the problem is in NP cap co-NP; (b) we show that for turn-based stochastic games the problem is co-NP-complete, both for finite-memory and infinite-memory strategies; and (c) we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above complexity results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of two qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games.

Cite as

Krishnendu Chatterjee and Nir Piterman. Combinations of Qualitative Winning for Stochastic Parity Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CONCUR.2019.6,
  author =	{Chatterjee, Krishnendu and Piterman, Nir},
  title =	{{Combinations of Qualitative Winning for Stochastic Parity Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.6},
  URN =		{urn:nbn:de:0030-drops-109089},
  doi =		{10.4230/LIPIcs.CONCUR.2019.6},
  annote =	{Keywords: Two Player Games, Stochastic Games, Parity Winning Conditions}
}

Document

DOI: 10.4230/LIPIcs.STACS.2015.211

Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics

Authors: Pablo Castro, Cecilia Kilmurray, and Nir Piterman

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract

We revisit a recently introduced probabilistic \mu-calculus and study an expressive fragment of it. By using the probabilistic quantification as an atomic operation of the calculus we establish a connection between the calculus and obligation games. The calculus we consider is strong enough to encode well-known logics such as pctl and pctl^*. Its game semantics is very similar to the game semantics of the classical mu-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NP\cap co-NP for its finite model checking procedure. Furthermore, we investigate a (relatively) well-behaved fragment of this calculus: an extension of pctl with fixed points. An important feature of this extended version of pctl is that its model checking is only exponential w.r.t. the alternation depth of fixed points, one of the main characteristics of Kozen's mu-calculus.

Cite as

Pablo Castro, Cecilia Kilmurray, and Nir Piterman. Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 211-223, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{castro_et_al:LIPIcs.STACS.2015.211,
  author =	{Castro, Pablo and Kilmurray, Cecilia and Piterman, Nir},
  title =	{{Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{211--223},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.211},
  URN =		{urn:nbn:de:0030-drops-49155},
  doi =		{10.4230/LIPIcs.STACS.2015.211},
  annote =	{Keywords: mu-calculus, probabilistic logics, model checking, game semantics}
}

Search Results

Documents authored by Piterman, Nir

Combinations of Qualitative Winning for Stochastic Parity Games

Abstract

Cite as

Tractable Probabilistic mu-Calculus That Expresses Probabilistic Temporal Logics

Abstract

Cite as

Thanks for your feedback!

Could not send message